home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / group_2.06.2 < prev    next >
Text File  |  1992-04-03  |  16KB  |  432 lines
  1. %%%
  2. %%% version 2.04.8
  3. %%%   initial version
  4. %%% version 2.05.1
  5. %%%   fixed assert_group_axiom so that it works when neither fixed_priority
  6. %%%     nor slidepriority is specified
  7. %%% version 2.05.2
  8. %%%   don't rewrite clauses in group dection
  9. %%%   fixed bug in assert_group_properties
  10. %%% version 2.05.3
  11. %%%   added support for Quintus Prolog
  12. %%% version 2.05.4
  13. %%%   rewrite rewrite rules after asserting group rewrite rule
  14. %%% version 2.05.5
  15. %%%   rewrite group axioms before asserting
  16. %%% version 2.06.0
  17. %%%   rewrite rewrite rules only once during group detection
  18. %%% version 2.06.1
  19. %%%   rewrite group rewrite rule before asserting
  20. %%%   rewrite replace rules
  21. %%% version 2.06.2
  22. %%%   fixed assert_group_axiom/1 to work when priority_bound is not set
  23. %%%
  24. %%% This is the code for group dectection.  A group with binary operation
  25. %%% f(X,Y), inverse g(X), and identity e is deceted if the following clauses
  26. %%% are asserted:
  27. %%% 
  28. %%%                f(f(X,Y),Z)=f(X,f(Y,Z))    associativity
  29. %%%                f(e,X)=X                   left identity
  30. %%%                f(g(X),X)=e                left inverse
  31. %%%
  32. %%% or if the following clauses are asserted:
  33. %%%
  34. %%%                f(f(X,Y),Z)=f(X,f(Y,Z))    associativity
  35. %%%                f(X,e)=X                   right identity
  36. %%%                f(X,g(X))=e                right inverse
  37. %%%
  38. %%% Note that the binary operation, inverse, and identity can be any
  39. %%% arbitrary term containing two, one, and zero distinct variables
  40. %%% respectively.
  41. %%%
  42. %%% When a new group is detected, the following clauses are asserted if not
  43. %%% already present:
  44. %%% 
  45. %%%           f(e,X)=X                    g(e)=e
  46. %%%           f(g(X),X)=e                 g(g(X))=X
  47. %%%           f(f(X,Y),Z)=f(X,f(Y,Z))     f(X,g(X))=e
  48. %%%           f(g(X),f(X,Y))=Y            f(X,f(g(X),Y))=Y
  49. %%%           f(X,e)=X                    g(f(X,Y))=f(g(Y),g(X))
  50. %%%
  51. %%% The group axioms are rewritten before being asserted.  If auto_orient is
  52. %%% set, rewrite rules are asserted for each the above equations if not
  53. %%% already present.  If replacement is set, the following repeated replace
  54. %%% rules with no context literals are also asserted if not already present:
  55. %%%
  56. %%%                     f(X,Y)=f(X,Z) --> Y=Z
  57. %%%                     f(Y,X)=f(Z,X) --> Y=Z
  58. %%%                     f(X,Y)=X      --> Y=e
  59. %%%                     f(Y,X)=X      --> Y=e
  60. %%%                     f(X,Y)=e      --> Y=g(X)
  61. %%%                     f(Y,X)=e      --> Y=g(X)
  62. %%%
  63. %%% When an old group is detected, if the new inverse operation g'(x) differs
  64. %%% from the old inverse operation g(x), the equation g'(x)=g(x) and its
  65. %%% associated rewrite rule are asserted.  If the new identity element e'
  66. %%% differs from the old identity element e, the equation e'=e and its
  67. %%% corresponding rewrite rule is asserted.  Check_group_found then fails.
  68.  
  69. %%%
  70. %%% Run_ground_detection checks for all possible groups.
  71. %%%
  72.     run_group_detection :-
  73.       not(group_detection),
  74.       !.
  75.     run_group_detection :-
  76.       cputime(TT1),
  77.       find_groups,
  78.       (group_rewrite_rule_asserted -> (
  79.         abolish(group_rewrite_rule_asserted,0),
  80.         rewrite_rewrite_rules(1),
  81.         rewrite_replace_rules
  82.       ); true),
  83.       cputime(TT2),
  84.       TT3 is TT2 - TT1,
  85.       write_line(5,'Group detection(s): ',TT3),
  86.       !.
  87.  
  88. %%%
  89. %%% Find_groups finds all possible groups as follows:
  90. %%%   1. For each asserted clause determine if it is the associativity axiom
  91. %%%      for some binary operation.
  92. %%%   2. If a clause is the associativity axiom for some binary operation,
  93. %%%      determine if the additional group axioms are present for the binary
  94. %%%      operation.
  95. %%%   3. If the additional group axioms are present, print a description of
  96. %%%      the group and assert the group properties.
  97. %%%
  98. %%% Note that new clauses are temporarily asserted as sent_G until all of
  99. %%% existing clauses have been examined.
  100. %%%
  101.     find_groups :-
  102.       sent_C(cl(_,_,by([S=T],V,V,_,_),_,_,_,_,_,_)),
  103.       is_associativity_axiom(S=T,Binop),
  104.       is_group(Binop,Inverse,Identity,Axiom_type),
  105.       check_group_found(Binop,Inverse,Identity),
  106.       print_group_description(Binop,Inverse,Identity),
  107.       assert_group_properties(Binop,Inverse,Identity,Axiom_type),
  108.       fail.
  109.     find_groups :-
  110.       retract(sent_G(C)),
  111.       assertz(sent_C(C)),
  112.       fail.
  113.     find_groups.
  114.  
  115. %%%
  116. %%% Is_associativity_axiom determines if an equation is an associativity axiom.
  117. %%% If the equation is an associativity axiom, the binary operation of the
  118. %%% associativity axiom is returned as a list of three terms:  the binary
  119. %%% operation, its first argument, and its second operation.
  120. %%%
  121.     is_associativity_axiom(S=T,Binop) :-
  122.       list_vars(S=T,[V1,V2,V3]),
  123.       get_subterms(S,Ss),
  124.       is_associativity_axiom_1(Ss,S=T,Binop),
  125.       !.
  126.     is_associativity_axiom_1([Op|_],S=T,[Op,X,Y]) :-
  127.       list_vars(Op,[X,Y]),
  128.       build_associativity_axiom([Op,X,Y],Assoc_axiom),
  129.       duplicate_clauses([S=T],[Assoc_axiom]),
  130.       !.
  131.     is_associativity_axiom_1([Op|_],S=T,[Op,Y,X]) :-
  132.       list_vars(Op,[X,Y]),
  133.       build_associativity_axiom([Op,Y,X],Assoc_axiom),
  134.       duplicate_clauses([S=T],[Assoc_axiom]),
  135.       !.
  136.     is_associativity_axiom_1([_|Ss],S=T,Binop) :-
  137.       !,
  138.       is_associativity_axiom_1(Ss,S=T,Binop).
  139.  
  140. %%%
  141. %%% Build_associativity_axiom creates the associativity axiom for a specified
  142. %%% binary operation.
  143. %%%
  144.     build_associativity_axiom([Op,X,Y],S=T) :-
  145.       asserta(baa_temp(Op,X,Y)),
  146.       baa_temp(S,Dummy1,V3),
  147.       baa_temp(Dummy1,V1,V2),
  148.       baa_temp(T,V1,Dummy2),
  149.       baa_temp(Dummy2,V2,V3),
  150.       retract(baa_temp(_,_,_)),
  151.       !.
  152.  
  153. %%%
  154. %%% Is_group determines if the group axioms for an associativity binary
  155. %%% operation are present.  If the group axioms are present, the inverse
  156. %%% operation of the group, the identity element of the group, and the type
  157. %%% group axioms found are returned.  The inverse operation is returned as
  158. %%% a list of two terms:  the inverse operation and its arguement.  The
  159. %%% identity element is returned as a list of one term:  the identity element.
  160. %%% The axioms type is returned as either l, indicating that the left inverse
  161. %%% and left identity axioms were used, or r, indicating that the right inverse
  162. %%% and right identity axioms were used.
  163. %%%
  164.     is_group([Op,X,Y],[Inv,Z],[Ident],Axiom_type) :-
  165.       asserta(ig_temp(Op,X,Y)),
  166.       is_group_1([Inv,Z],[Ident],Axiom_type).
  167.     is_group(_,_,_,_) :-
  168.       retract(ig_temp(_,_,_)),
  169.       !,
  170.       fail.
  171.     is_group_1([Inv,Z],[Ident],l) :-
  172.       ig_temp(S1,Inv,Z),
  173.       sent_C(cl(_,_,by([S1=Ident],V11,V12,_,_),_,_,_,_,_,_)),
  174.       unify_lists(V11,V12),
  175.       var(Z),
  176.       list_vars(Inv,[Z]),
  177.       list_vars(Ident,[]),
  178.       sent_C(cl(_,_,by([S2=A],V21,V22,_,_),_,_,_,_,_,_)),
  179.       unify_lists(V21,V22),
  180.       var(A).
  181.     is_group_1([Inv,Z],[Ident],l) :-
  182.       ig_temp(S1,Z,Inv),
  183.       sent_C(cl(_,_,by([S1=Ident],V11,V12,_,_),_,_,_,_,_,_)),
  184.       unify_lists(V11,V12),
  185.       var(Z),
  186.       list_vars(Inv,[Z]),
  187.       list_vars(Ident,[]),
  188.       ig_temp(S2,A,Ident),
  189.       sent_C(cl(_,_,by([S2=A],V21,V22,_,_),_,_,_,_,_,_)),
  190.       unify_lists(V21,V22),
  191.       var(A).
  192.  
  193. %%%
  194. %%% Check_group_found determines if a group has already been found during the
  195. %%% current session.  If it has not, check_group_found saves a description of
  196. %%% the group.  Otherwise, if the new inverse operation g'(x) differs from the
  197. %%% old inverse operation g(x), the equation g'(x)=g(x) and its associated 
  198. %%% rewrite rule are asserted.  If the new identity element e' differs from the
  199. %%% old identity element e, the equation e'=e and its corresponding rewrite
  200. %%% rule is asserted.  Check_group_found then fails.
  201. %%%
  202.  
  203.     check_group_found([Binop,X,Y],[Inverse,Z],[Identity]) :-
  204.       const_list([X,Y,Z|_]),
  205.       group_descr([Binop,X,Y],[Inverse,Z],[Identity]),
  206.       !,
  207.       fail.
  208.     check_group_found([Binop,X,Y],[Inverse1,Z],[Identity1]) :-
  209.       assert(cgf_temp([Binop,X,Y])),
  210.       const_list([X,Y|_]),
  211.       group_descr([Binop,X,Y],[Inverse2,Z],[Identity2]),
  212.       cgf_temp(Binop1),
  213.       print_group_description(Binop1,[Inverse1,Z],[Identity1]),
  214.       assert(group_descr(Binop1,[Inverse1,Z],[Identity1])),
  215.       check_group_found_1(Inverse1,Inverse2),
  216.       check_group_found_2(Identity1,Identity2),
  217.       retract(cgf_temp(_)),
  218.       !,
  219.       fail.
  220.     check_group_found(Binop,Inverse,Identity) :-
  221.       retract(cgf_temp(_)),
  222.       assert(group_descr(Binop,Inverse,Identity)),
  223.       !.
  224.     check_group_found_1(Inverse1,Inverse2) :-
  225.       Inverse1\==Inverse2,
  226.       assert_group_axiom(Inverse2=Inverse1),
  227.       !.
  228.     check_group_found_1(_,_).
  229.     check_group_found_2(Identity1,Identity2) :-
  230.       Identity1\==Identity2,
  231.       assert_group_axiom(Identity2=Identity1),
  232.       !.
  233.     check_group_found_2(_,_).
  234.  
  235. %%%
  236. %%% Print_group_description prints a description of a group.
  237. %%%
  238.     print_group_description(Binop,Inverse,[Identity]) :-
  239.       write_line(10,'*** Group detected ***'),
  240.       not(not(print_group_description_1(Binop))),
  241.       not(not(print_group_description_2(Inverse))),
  242.       write_line(15,'Identity:         ',Identity),
  243.       !.
  244.     print_group_description_1([Op,'X','Y']) :-
  245.       write_line(15,'Binary operation: ',Op),
  246.       !.
  247.     print_group_description_2([Op,'X']) :-
  248.       write_line(15,'Inverse:          ',Op),
  249.       !.
  250.  
  251. %%%
  252. %%% Assert_group_properties asserts the group properties:  equations, rewrite
  253. %%% rules, and replace rules.
  254. %%%
  255.     assert_group_properties([Binop,X,Y],[Inverse,Z],[Identity],Axiom_type) :-
  256.       assert(agp_binop(Binop,X,Y)),
  257.       assert(agp_inverse(Inverse,Z)),
  258.       assert(agp_identity(Identity)),
  259.       assert_group_properties_1(Axiom_type),
  260.       retract(agp_binop(_,_,_)),
  261.       retract(agp_inverse(_,_)),
  262.       retract(agp_identity(_)),
  263.       !.
  264.     assert_group_properties_1(l) :-
  265.       assert_right_group_axioms,
  266.       assert_other_group_axioms,
  267.       assert_group_replace_rules,
  268.       !.
  269.     assert_group_properties_1(r) :-
  270.       assert_left_group_axioms,
  271.       assert_other_group_axioms,
  272.       assert_group_replace_rules,
  273.       !.
  274.  
  275. %%%
  276. %%% Assert_left_group_axioms asserts the left inverse and left identity
  277. %%% axioms and corresponding rewrite rules for a specified group.  
  278. %%% Assert_right_group_axioms assumes that the group operations have been
  279. %%% asserted as agp_binop, agp_inverse, and agp_indentity.
  280. %%%
  281.     assert_left_group_axioms :-
  282.       agp_binop(S1,Temp1,X),
  283.       agp_inverse(Temp1,X),
  284.       agp_identity(Identity),
  285.       assert_group_axiom(S1=Identity),
  286.       agp_binop(S2,Identity,X),
  287.       assert_group_axiom(S2=X),
  288.       !.
  289.  
  290. %%%
  291. %%% Assert_right_group_axioms asserts the right inverse and right identity
  292. %%% axioms and corresponding rewrite rules for a specified group.  
  293. %%% Assert_right_group_axioms assumes that the group operations have been
  294. %%% asserted as agp_binop, agp_inverse, and agp_indentity.
  295. %%%
  296.     assert_right_group_axioms :-
  297.       agp_binop(S1,X,Temp1),
  298.       agp_inverse(Temp1,X),
  299.       agp_identity(Identity),
  300.       assert_group_axiom(S1=Identity),
  301.       agp_binop(S2,X,Identity),
  302.       assert_group_axiom(S2=X),
  303.       !.
  304.  
  305. %%%
  306. %%% Assert_other_group_axioms asserts the following axioms and corresponding
  307. %%% rewrite rules for a specified group:
  308. %%%      f(g(X),f(X,Y))=Y
  309. %%%      g(e)=e
  310. %%%      g(g(X))=X
  311. %%%      f(X,f(g(X),Y))=Y
  312. %%%      g(f(X,Y))=f(g(Y),g(X))
  313. %%% The group axioms are rewritten before being asserted.
  314. %%% Assert_other_group_axioms assumes that the group operations have been
  315. %%% asserted as agp_binop, agp_inverse, and agp_indentity.
  316. %%%
  317.     assert_other_group_axioms :-
  318.       agp_binop(S1,Temp1,Temp2),
  319.       agp_inverse(Temp1,X),
  320.       agp_binop(Temp2,X,Y),
  321.       assert_group_axiom(S1=Y),
  322.       agp_inverse(S2,Identity),
  323.       agp_identity(Identity),
  324.       assert_group_axiom(S2=Identity),
  325.       agp_inverse(S3,Temp3),
  326.       agp_inverse(Temp3,X),
  327.       assert_group_axiom(S3=X),
  328.       agp_binop(S4,X,Temp4),
  329.       agp_binop(Temp4,Temp5,Y),
  330.       agp_inverse(Temp5,X),
  331.       assert_group_axiom(S4=Y),
  332.       agp_inverse(S5,Temp6),
  333.       agp_binop(Temp6,X,Y),
  334.       agp_binop(T5,Temp7,Temp8),
  335.       agp_inverse(Temp7,Y),
  336.       agp_inverse(Temp8,X),
  337.       assert_group_axiom(S5=T5),
  338.       !.
  339.  
  340. %%%
  341. %%% Assert_group_axiom asserts a group axiom if the axiom is not already
  342. %%% asserted and its priority is not too large.  Also, assert_group_axiom
  343. %%% asserts the corresponding rewrite rule if the equation is asserted and
  344. %%% auto_orient is set.  Rewrite group axiom before asserting it.
  345. %%%
  346.     assert_group_axiom(Axiom) :-
  347.       (constrained_rewriting -> (
  348.         (restricted_rewrite -> (
  349.           abolish(restricted_rewrite,0),
  350.           rewrite_clause_with_constraint([Axiom],_,_,[],Cts),
  351.           assert(restricted_rewrite)
  352.         ); (
  353.           rewrite_clause_with_constraint([Axiom],_,_,[],Cts)
  354.         )),
  355.         assert_group_axiom_1(Cts)
  356.       ); (
  357.         (restricted_rewrite -> (
  358.           abolish(restricted_rewrite,0),
  359.           rewrite_clause_np([Axiom],_,_,0,[Axiom1],_),
  360.           assert(restricted_rewrite)
  361.         ); (
  362.           rewrite_clause_np([Axiom],_,_,0,[Axiom1],_)
  363.         )),
  364.         assert_group_axiom_2([Axiom1])
  365.       )).
  366.     assert_group_axiom_1([]) :- !.
  367.     assert_group_axiom_1([[Axiom,_,_]|Cts]) :-
  368.       assert_group_axiom_2(Axiom),
  369.       assert_group_axiom_1(Cts).
  370.     assert_group_axiom_2([S=T]) :-
  371.       vars_tail([S=T],V),
  372.       clause_size([S=T],CSize),
  373.       (not(duplicate_clause_C(CSize,[S=T],V)) -> (
  374.         linearize_term([S=T],C,V1,V2),
  375.         vars_literals([S=T],W),
  376.         compute_V_lits(W,0,NLits),
  377.         set_user_support(C,Sup1),
  378.         set_sr_status(Sup1,C,Sp,Ds),
  379.         list_of_Ns(C,0,Dis),
  380.         calculate_priority_clause(C,Sp,Ds,Pr),
  381.         ((not(priority_bound(_));
  382.             (priority_bound(PrioBound),check_prioritybound(Pr,PrioBound))) -> (
  383.           assertz(sent_G(cl(CSize,NLits,by(C,V1,V2,V,W),0,Sp,Ds,0,Dis,Pr))),
  384.           generate_rewrite_rule([S=T],F),
  385.           (F==1 -> (
  386.             assert_once(group_rewrite_rule_asserted)
  387.           ); true)
  388.         ); true)
  389.       ); true).
  390.  
  391. %%%
  392. %%% If replacement is set, assert_group_replace_rules asserts the following
  393. %%% repeated replace rules with no context literals:
  394. %%%           f(X,Y)=f(X,Z) --> Y=Z
  395. %%%           f(Y,X)=f(Z,X) --> Y=Z
  396. %%%           f(X,Y)=X      --> Y=e
  397. %%%           f(Y,X)=X      --> Y=e
  398. %%%           f(X,Y)=e      --> Y=g(X)
  399. %%%           f(Y,X)=e      --> Y=g(X)
  400. %%% Assert_group_replace_rules assumes that the group operations have been
  401. %%% asserted as agp_binop, agp_inverse, and agp_indentity.
  402. %%%
  403.     assert_group_replace_rules :-
  404.       replacement,
  405.       agp_binop(S1,X,Y),
  406.       agp_binop(T1,X,Z),
  407.       assert_group_replace_rule(S1=T1,Y=Z),
  408.       agp_binop(S2,Y,X),
  409.       agp_binop(T2,Z,X),
  410.       assert_group_replace_rule(S2=T2,Y=Z),
  411.       agp_identity(Identity),
  412.       assert_group_replace_rule(S1=X,Y=Identity),
  413.       assert_group_replace_rule(S2=X,Y=Identity),
  414.       agp_inverse(T3,X),
  415.       assert_group_replace_rule(S1=Identity,Y=T3),
  416.       assert_group_replace_rule(S2=Identity,Y=T3),
  417.       !.
  418.     assert_group_replace_rules.
  419.  
  420. %%%
  421. %%% Assert_group_replace_rule asserts a single repeated replace rule with no
  422. %%% context literals for a group.
  423. %%%
  424.     assert_group_replace_rule(L1,L2) :-
  425.       negate(L1,L1n),
  426.       vars_tail([L1n,L2],V),
  427.       not(duplicate_repeated_replace_rule([L1n,L2],V)),
  428.       vars_literals([L1n,L2],W),
  429.       assertz(replace_rule_1([L1n,L2],V,W,[1,0],[0,0])),
  430.       !.
  431.     assert_group_replace_rule(_,_).
  432.